;;;===========================================================================
;;;
;;; Subject: Generator of simplicial complex from a digital
;;;          image
;;;
;;;---------------------------------------------------------------------------
;;;
;;; Jónathan Heras Vicente
;;; Beginning date: 09-12-10
;;; End date: 13-12-10
;;;
;;;===========================================================================


(in-package "ACL2")


;;;---------------------------------------------------------------------------
;;;
;;; Main definitions
;;;
;;;---------------------------------------------------------------------------

(defun list-0-1 (list)
  (if (endp list)
      (equal list nil)
    (if (endp (cdr list))
	(and (equal (cdr list) nil)
	     (or (equal (car list) 0) (equal (car list) 1)))
      (and (or (equal (car list) 0) (equal (car list) 1))
	   (list-0-1 (cdr list))))))

;; (list-0-1 '(1 0 1 0 1 0))
  
(defun 2d-imagep (list)
  (if (endp list)
      (equal list nil)
    (and (list-0-1 (car list))
	 (2d-imagep (cdr list)))))
    


(defun genera-facets-i-j (i j)
  (list (list (list i j) (list (1+ i) j) (list (1+ i) (1+ j)))
	(list (list i j) (list i (1+ j)) (list (1+ i) (1+ j))))
  )


(defun genera-facets-list (list i j)
  (if (endp list)
      nil
    (if (equal (car list) 1)
	(append (genera-facets-i-j i j) 
		(genera-facets-list (cdr list) (1+ i) j))
      (genera-facets-list (cdr list) (1+ i) j))))


(defun genera-facets-image-aux (list j)
  (if (endp list)
      nil
    (append (genera-facets-list (car list) 0 j)
	    (genera-facets-image-aux (cdr list) (1+ j)))))

(defun genera-facets-image (list)
  (genera-facets-image-aux list 0))


;;; (genera-facets-image '((1 0) (0 1)))




;;;---------------------------------------------------------------------------
;;;
;;; Property: genera-facets-image generates a list of simplexes over (N,N)
;;;
;;;---------------------------------------------------------------------------

(defun l-ord (list1 list2)
  (cond ((and (endp list1) (endp list2)) nil)
	((endp list1) t)
	((endp list2) nil)
	((< (car list1) (car list2)) t)
	(t (l-ord (cdr list1) (cdr list2)))))
 

(defun nat-listp (list)
  (if (endp list)
      (equal list nil)
    (and (natp (car list))
	 (nat-listp (cdr list)))))


(defun simplex-p (list)
  (if (endp list)
      (equal list nil)
    (if (endp (cdr list))
	(and (equal (cdr list) nil) (nat-listp (car list)))
      (and (nat-listp (car list)) (nat-listp (cadr list))
	   (l-ord (car list) (cadr list))
	   (simplex-p (cdr list))))))
	

(defun simplex-N-N-p (list)
  (and (equal (len list) 3)
       (simplex-p list))
  )


(defun list-of-simplexes-N-N-p (lol)
  (if (endp lol)
      (equal lol nil)
    (and (simplex-N-N-p (car lol))
	 (list-of-simplexes-N-N-p (cdr lol)))))


(defthm append-list-of-simplexes-n-n-p
  (implies (and (list-of-simplexes-n-n-p x)
		(list-of-simplexes-n-n-p y))
	   (list-of-simplexes-n-n-p (append x y))))


(defthm genera-facets-list-generates-list-of-simplexes-n-n-p
  (implies (and (list-0-1 x)
		(natp i)
		(natp j))
	   (list-of-simplexes-n-n-p (genera-facets-list x i j))))

(defthm genera-facets-image-generates-list-of-simplexes-n-n-p-aux
  (implies (and (2d-imagep x)
		(natp j))
	   (list-of-simplexes-n-n-p (genera-facets-image-aux x j))))

(defthm genera-facets-image-generates-list-of-simplexes-n-n-p
  (implies (2d-imagep image)
	   (list-of-simplexes-n-n-p (genera-facets-image image))))


;;;---------------------------------------------------------------------------
;;;
;;; Property: The number of elements obtained from 
;;; genera-facets-image is equal to 2 times the number
;;; of ones of the list
;;;
;;;---------------------------------------------------------------------------

(encapsulate
 ()

(defun count-1-list (list)
  (if (endp list)
      0
    (if (equal (car list) 1)
	(1+ (count-1-list (cdr list)))
      (count-1-list (cdr list)))))


(defun count-1-lol (lol)
  (if (endp lol)
      0
    (+ (count-1-list (car lol))
       (count-1-lol (cdr lol)))))


(local (defthm facets=2*number-of-1-list
  (implies (list-0-1 x)
	   (equal (len (genera-facets-list x i j))
		  (* 2 (count-1-list x))))))


(local (defthm len-append
  (implies (consp x)
	   (equal (+ (len x) (len y))
		  (len (append x y))))))

(local (defthm facets=2*number-of-1-aux
  (implies (2d-imagep image)
	   (equal (len (genera-facets-image-aux image k))
		  (* 2 (count-1-lol image))))
  :hints (("Subgoal *1/3''" :use
	   ((:instance len-append (x (GENERA-FACETS-LIST (CAR IMAGE) 0 K))
		       (y (GENERA-FACETS-IMAGE-AUX (CDR IMAGE)
                                                      (+ 1 K)))
		       )
	    (:instance facets=2*number-of-1-list (x (car image))
		       (i 0)
		       (j k)))))))


(defthm facets=2*number-of-1
  (implies (2d-imagep image)
	   (equal (len (genera-facets-image image))
		  (* 2 (count-1-lol image)))))

)


;;;---------------------------------------------------------------------------
;;;
;;; Additional definitions for the proofs
;;;
;;;---------------------------------------------------------------------------

(defun list-up (simplex)
  (let ((i (car (car simplex)))
	(j (cadr (car simplex))))
  (list (list i j) (list (1+ i) j) (list (1+ i) (1+ j)))))

(defun list-down (simplex)
  (let ((i (car (car simplex)))
	(j (cadr (car simplex))))
  (list (list i j) (list i (1+ j)) (list (1+ i) (1+ j)))))


(defun member-list-up (simplex)
  (let ((i (car (car simplex)))
	(j (cadr (car simplex))))
  (equal (list (1+ i) j) (cadr simplex))))

(defun member-list-down (simplex)
  (let ((i (car (car simplex)))
	(j (cadr (car simplex))))
  (equal (list i (1+ j)) (cadr simplex))))

(defun list-up-i-j (i j)
  (list (list i j) (list (1+ i) j) (list (1+ i) (1+ j))))

(defun list-down-i-j (i j)
  (list (list i j) (list i (1+ j)) (list (1+ i) (1+ j))))

;;;---------------------------------------------------------------------------
;;;
;;; Additional lemmas
;;;
;;;---------------------------------------------------------------------------

(defthm list-0-1-not
  (implies (not (list-0-1 (cdr x)))
	   (not (list-0-1 x))))

(defthm 2d-imagep-not
  (implies (not (2d-imagep (cdr image)))
	   (not (2d-imagep image))))

(defthm member-equal-append
  (implies (member-equal a b)
	   (member-equal a (append c b))))

(defthm append-member-not
  (implies (and (not (member-equal a c))
		(member-equal a (append b c)))
	   (member-equal a b)))

(defthm member-equal-append-2
  (implies (member-equal a b)
	   (member-equal a (append b c))))

(defthm list-down-list-up
  (implies (and (natp i)
		(natp j))
	   (equal (list-down-i-j i j)
		  (list-down (list-up-i-j i j)))))


;;;---------------------------------------------------------------------------
;;;
;;; Property: Verification of the correctness of the
;;; algorithm genera-facets-image
;;;
;;;---------------------------------------------------------------------------

;;;***************************************************************************
;;;
;;; First and second well definition theorems
;;;
;;;***************************************************************************


(defthm member-equal-genera-facets-image-aux
  (implies (and (consp image)
		(member-equal a (genera-facets-image-aux (cdr image) (1+ j))))
	   (member-equal a (genera-facets-image-aux image j))))


(defthm member-equal-genera-facets-list
  (implies (and (member-equal simplex (genera-facets-list a i j))
		(member-list-up simplex))
	   (member-equal (list-down simplex) (genera-facets-list a i j)))
	   )

(defthm member-equal-genera-facets-list-down
  (implies (and (member-equal simplex (genera-facets-list a i j))
		(member-list-down simplex))
	   (member-equal (list-up simplex) (genera-facets-list a i j)))
	   )

(defthm not-member-equal-list-image-aux
  (implies (and (consp b)
		(not (member-equal a (genera-facets-image-aux (cdr b) (1+ j))))
		(member-equal a (genera-facets-image-aux b j)))
	   (member-equal a (genera-facets-list (car b) 0 j))))
 
(defthm member-equal-genera-facets-list-member-equal-image-aux
  (implies (member-equal a (genera-facets-list (car b) 0 j))
	   (member-equal a (genera-facets-image-aux b j))))

(defthm well-defined-genera-facets-image-1-aux
  (implies (and (2d-imagep image)
		(member-equal simplex (genera-facets-image-aux image j))
		(member-list-up simplex))
	   (member-equal (list-down simplex)
			 (genera-facets-image-aux image j)))
  :hints (("Goal" :in-theory (disable genera-facets-list list-down member-list-up))))

(defthm well-defined-genera-facets-image-2-aux
  (implies (and (2d-imagep image)
		(member-equal simplex (genera-facets-image-aux image j))
		(member-list-down simplex))
	   (member-equal (list-up simplex)
			 (genera-facets-image-aux image j)))
  :hints (("Goal" :in-theory (disable genera-facets-list list-up member-list-down))))


(defthm well-defined-genera-facets-image-1
  (implies (and (2d-imagep image)
		(member-equal simplex (genera-facets-image image))
		(member-list-up simplex))
	   (member-equal (list-down simplex)
			 (genera-facets-image image)))
  :hints (("Goal" :in-theory (disable genera-facets-list list-down member-list-up))))
	 

(defthm well-defined-genera-facets-image-2
  (implies (and (2d-imagep image)
		(member-equal simplex (genera-facets-image image))
		(member-list-down simplex))
	   (member-equal (list-up simplex)
			 (genera-facets-image image)))
  :hints (("Goal" :in-theory (disable genera-facets-list list-up member-list-down))))


;;;***************************************************************************
;;;
;;; Third well definition theorem
;;;
;;;***************************************************************************

   
(defthm natp-member-equal-genera-facets-list
  (implies (and (list-0-1 x)
		(natp l)
		(natp k)
		(member-equal simplex (genera-facets-list x k l)))
	   (natp (caar simplex))))


(defthm caar>=k-member-equal-genera-facets-list
  (implies (and (list-0-1 x)
		(natp l)
		(natp k)
		(member-equal simplex (genera-facets-list x k l)))
	   (<= k (caar simplex))))

(defthm caar<len-member-equal-genera-facets-list
  (implies (and (list-0-1 x)
		(natp l)
		(natp k)
		(member-equal simplex (genera-facets-list x k l)))
	   (< (caar simplex) (+ (len x) k))))
		

(defthm member-genera-facets-list-cdr
  (implies (and (list-0-1 x)
		(natp k)
		(natp l)
		(member-equal simplex (genera-facets-list (cdr x) (1+ k) l)))
	   (member-equal simplex (genera-facets-list x k l))))


(defthm nth-cdr
  (implies (and (natp i)
		(> i 0))
	   (equal (nth (- i 1) (cdr x))
		  (nth i x))))


(defthm auxiliar-1
  (implies (and (natp i)
		(natp j)
		(< i j))
	   (equal (+ (- (+ 1 i)) j)
		  (- (- j i) 1)))
  :rule-classes nil)

(defthm auxiliar-2
  (implies (and (natp i)
		(natp j)
		(< i j))
	   (equal (+ (- i) j)
		  (- j i)))
  :rule-classes nil)


(defthm auxiliar-3
  (implies (and (natp i)
		(natp j)
		(< i j))
	   (equal (nth (+ (- (+ 1 i)) j) (cdr x))
		  (nth (+ (- i) j) x)))
  :hints (("Goal"  :use ((:instance auxiliar-1)
			 (:instance auxiliar-2)
			 (:instance nth-cdr (i (- j i)))))))

(defthm transitive
  (implies (and (natp x)
		(natp y)
		(<= (1+ x) y))
	   (< x y)))


(defthm caar>k-member-equal-genera-facets-list-cdr
  (implies (and (list-0-1 x)
		(natp l)
		(natp k)
		(member-equal simplex (genera-facets-list x (1+ k) l)))
	   (< k (caar simplex)))
  :hints (("Goal" :use ((:instance natp-member-equal-genera-facets-list
				   (k (1+ k)))
			(:instance caar>=k-member-equal-genera-facets-list
				  (k (1+ k)))
			(:instance transitive (x k) (y (caar simplex)))))))


(defthm facets-list-well-defined-aux-1
  (implies (and (list-0-1 (cdr x))
		(equal (car x) 0)
		(natp l)
		(natp k)
		(equal (nth (+ (- (+ 1 K)) (CAAR SIMPLEX)) (cdr x)) 1)
		(member-equal simplex (genera-facets-list (cdr x) (1+ k) l)))
	   (equal (nth (+ (- k) (caar simplex)) x) 1))
    :hints (("Goal" 
	   :use ((:instance natp-member-equal-genera-facets-list (x (cdr x)) (k (1+ k)))
		 (:instance caar>=k-member-equal-genera-facets-list (x (cdr x)) (k (1+ k)))
		 (:instance caar>k-member-equal-genera-facets-list-cdr)))
	  ))

(defthm facets-list-well-defined-aux-2
  (implies (and (list-0-1 (cdr x))
		(equal (car x) 1)
		(natp l)
		(natp k)
		(equal (nth (+ (- (+ 1 K)) (CAAR SIMPLEX)) (cdr x)) 1)
		(member-equal simplex (genera-facets-list (cdr x) (1+ k) l)))
	   (equal (nth (+ (- k) (caar simplex)) x) 1))
    :hints (("Goal" 
	   :use ((:instance natp-member-equal-genera-facets-list (x (cdr x)) (k (1+ k)))
		 (:instance caar>=k-member-equal-genera-facets-list (x (cdr x)) (k (1+ k)))
		 (:instance caar>k-member-equal-genera-facets-list-cdr)))
	  ))

    
(defthm facets-list-well-defined
  (implies (and (list-0-1 x)
		(natp l)
		(natp k)
		(member-equal simplex (genera-facets-list x k l)))
	   (equal (nth (- (caar simplex) k) x) 1)))
 

(defthm natp-cadar-member-equal-genera-facets-list
  (implies (and (list-0-1 x)
		(natp l)
		(natp k)
		(member-equal simplex (genera-facets-list x k l)))
	   (natp (cadar simplex))))

(defthm cadar>=k-member-equal-genera-facets-list
  (implies (and (list-0-1 x)
		(natp l)
		(natp k)
		(member-equal simplex (genera-facets-list x k l)))
	   (<= l (cadar simplex))))

(defthm natp-cadar-member-equal-genera-facets-image-aux
  (implies (and (2d-imagep x)
		(natp k)
		(member-equal simplex (genera-facets-image-aux x k)))
	   (natp (cadar simplex)))
  :hints (("Subgoal *1/2" :use
	   (:instance natp-cadar-member-equal-genera-facets-list
		      (x (car x))
		      (k 0) (l k)))))

(defthm caar>=k-member-equal-genera-facets-image-aux
  (implies (and (2d-imagep x)
		(natp k)
		(member-equal simplex (genera-facets-image-aux x k)))
	   (<= k (cadar simplex)))
  :hints (("Subgoal *1/2" :use
	   (:instance cadar>=k-member-equal-genera-facets-list
		      (x (car x))
		      (k 0) (l k)))))

(defthm cadar=k-member-equal-genera-facets-list
  (implies (and (list-0-1 x)
		(natp l)
		(natp k)
		(member-equal simplex (genera-facets-list x k l)))
	   (equal (cadar simplex) l)))

(defthm genera-facets-well-defined-aux-help-1
  (implies (and (2d-imagep (cdr image))
		(list-0-1 (car image))
		(natp k)
		(member-equal simplex (genera-facets-list (car image) 0 k))
		)
	   (equal (nth (caar simplex) (nth (+ (-  k) (cadar simplex)) image))
		  1))
  :hints (("Goal" :use
	   ((:instance cadar=k-member-equal-genera-facets-list
		       (x (car image)) (k 0) (l k))
	    (:instance facets-list-well-defined
		       (x (car image)) (k 0) (l k))))))

(defthm genera-facets-well-defined-aux-help-2
  (implies
     (and (or (not (and (2d-imagep (cdr image))
                        (natp (+ 1 k))
                        (member-equal simplex
                                      (genera-facets-image-aux (cdr image)
                                                               (+ 1 k)))))
              (equal (nth (caar simplex)
                          (nth (+ (cadar simplex) (- (+ 1 k)))
                               (cdr image)))
                     1))
          (2d-imagep image)
          (natp k)
          (member-equal simplex
                        (genera-facets-image-aux image k)))
     (equal (nth (caar simplex)
                 (nth (+ (cadar simplex) (- k)) image))
            1)))

(defthm genera-facets-well-defined-aux
  (implies (and (2d-imagep image)
		(natp k)
		(member-equal simplex (genera-facets-image-aux image k)))
	   (equal (nth (caar simplex) (nth (- (cadar simplex) k) image)) 1)
	   )
  :hints (("Subgoal *1/2" :use ((:instance genera-facets-well-defined-aux-help-2 )))))


(defthm well-defined-genera-facets-image-3
  (implies (and (2d-imagep image)		
		(member-equal simplex (genera-facets-image image)))
	   (equal (nth (caar simplex) (nth (cadar simplex) image))
		  1))
  :hints (("Goal" :use (:instance genera-facets-well-defined-aux (k 0)))))


;;;---------------------------------------------------------------------------
;;;
;;; Property: Verification of the completeness of the
;;; algorithm genera-facets-image
;;;
;;;---------------------------------------------------------------------------

(encapsulate ()

(local (defthm member-list-up-list-up-i-j
  (member-list-up (list-up-i-j i j))))

(local (defthm member-list-down-list-down-i-j
  (member-list-down (list-down-i-j i j))))


(local (defthm --1-i-1-l
  (implies (and (natp i)
		(natp l))
	   (equal (+ -1 i 1 l)
		  (+ i l)))))
		
(local (defthm in-facets-list
  (implies (and (list-0-1 x)
		(natp i)
		(natp l)
		(natp k)
		(equal (nth i x) 1))
	   (member-equal (list-up-i-j (+ i l) k) (genera-facets-list x l k))
  )))


(local (defthm in-facets-list-case
  (implies (and (list-0-1 x)
		(natp i)
		(natp k)
		(equal (nth i x) 1))
	   (member-equal (list-up-i-j i k) (genera-facets-list x 0 k))
  )
  :hints (("Goal" :use ((:instance in-facets-list (l 0)))))))


(local (defthm well-defined-genera-facets-image-completo-aux
  (implies (and (2d-imagep image)
		(natp i)
		(natp j)
		(natp k)
		(equal (nth i (nth j image)) 1))
	   (member-equal (list-up-i-j i (+ j k)) (genera-facets-image-aux image k))
  )
:hints (("Goal" :in-theory (disable list-up-i-j)))))
 

(defthm well-defined-genera-facets-image-completeness
  (implies (and (2d-imagep image)
		(natp i)
		(natp j)
		(equal (nth i (nth j image)) 1))
	   (member-equal (list-up-i-j i j) (genera-facets-image image))
  )
  :hints (("Goal" :in-theory (disable list-up-i-j)
	   :use (:instance well-defined-genera-facets-image-completo-aux
			   (k 0)))))

(defthm well-defined-genera-facets-image-completeness-2
  (implies (and (2d-imagep image)
		(natp i)
		(natp j)
		(equal (nth i (nth j image)) 1))
	   (member-equal (list-down-i-j i j) (genera-facets-image image))
  )
  :hints (("Goal" :in-theory (disable list-up-i-j)
	   :use ((:instance well-defined-genera-facets-image-1
			    (simplex (list-up-i-j i j)))
		 (:instance well-defined-genera-facets-image-completeness)))))
)
